Nuprl Lemma : monoid_hom_id
13,42
postcript
pdf
g
,
h
:GrpSig,
f
:MonHom(
g
,
h
).
f
(e) = e
|
h
|
latex
Up
groups
1
Definitions of Statement
IsMonHom{
M1
,
M2
}(
f
)
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
IsMonHom{
M1
,
M2
}(
f
)
Lemmas
grp
sig
wf
,
monoid
hom
wf
,
monoid
hom
properties
origin